ePMC

Benchmark
Model:crowds v.1 (DTMC)
Parameter(s)TotalRuns = 5, CrowdSize = 20
Property:positive (prob-reach)
Invocation (default)
java -Xms10240m -Xmx10240m -jar ./root/epmc-standard.jar check --model-input-files crowds.prism --model-input-type prism --property-input-files crowds.props --property-input-names positive --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const TotalRuns=5,CrowdSize=20
Execution
Walltime:64.05401825904846s
Return code:0
Relative Error:4.2529298585697195e-06
Log
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property positive
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-states-explored 21566 21564
build-model-states-explored 54390 32826
build-model-states-explored 90791 36401
build-model-states-explored 130372 39581
build-model-states-explored 194037 63665
build-model-states-explored 223255 29218
build-model-states-explored 245588 22333
build-model-states-explored 266232 20644
build-model-states-explored 299217 32985
build-model-states-explored 363238 64021
build-model-states-explored 401907 38669
build-model-states-explored 437462 35555
build-model-states-explored 481981 44518
build-model-states-explored 538362 56381
build-model-states-explored 606762 68400
build-model-states-explored 635212 28450
build-model-states-explored 652716 17504
build-model-states-explored 673346 20629
build-model-states-explored 694151 20805
build-model-states-explored 718257 24107
build-model-states-explored 740166 21909
build-model-states-explored 762480 22314
build-model-states-explored 784858 22378
build-model-states-explored 842183 57325
build-model-states-explored 905343 63159
build-model-states-explored 968933 63591
build-model-states-explored 1040515 71581
build-model-states-explored 1087244 46729
build-model-states-explored 1154121 66876
build-model-states-explored 1207668 53548
build-model-states-explored 1276863 69195
build-model-states-explored 1340724 63861
build-model-states-explored 1361450 20726
build-model-states-explored 1378034 16584
build-model-states-explored 1399856 21822
build-model-states-explored 1421795 21939
build-model-states-explored 1443548 21753
build-model-states-explored 1465410 21862
build-model-states-explored 1487330 21920
build-model-states-explored 1509161 21831
build-model-states-explored 1531021 21859
build-model-states-explored 1552769 21749
build-model-states-explored 1574614 21845
build-model-states-explored 1596500 21886
build-model-states-explored 1618201 21701
build-model-states-explored 1639860 21659
build-model-states-explored 1661941 22081
build-model-states-explored 1684072 22131
build-model-states-explored 1706008 21936
build-model-states-explored 1727942 21934
build-model-states-explored 1768515 40572
build-model-states-explored 1848287 79772
build-model-states-explored 1927635 79349
build-model-states-explored 2006946 79311
build-model-done 2061951 54
iterating
iterating-progress-unbounded 39 0.06283594089326872 1
iterating-progress-unbounded 84 0.0010509165505031173 2
iterating-progress-unbounded 130 3.5953868433173546E-6 3
iterating-done 141 3
model-checking-done 62
command-check-result-is 0.08606868839085893 positive